p:FinProbSpace, f:(), X:(n:RandomVariable(p;f(n))), s, k:.
(n:, i:{0..n}. f(i) < f(n))
 (n:.
 E(f(n);X(n)) = 0   & E(f(n);(x.x * x) o X(n)) = s & E(f(n);(x.(x * x) * x * x) o X(n)) = k)
 (n:, i:{0..n}. rv-disjoint(p;f(n);X(i);X(n)))
 (B:
 ((0  B & (n:. E(f(n);(x.(x * x) * x * x) o rv-partial-sum(n;i.X(i)))  B * n * n))) 

latex

Definitions

a < b, x(s), r  s, #$n, x:A. B(x), rv-disjoint(p;n;X;Y), E(n;F), (x.F(x)) o X, x. t(x), r * s, RandomVariable(p;n), T, True, <a, b>, f(a), ||as||, type List, Top, Outcome, FinProbSpace, Type, x,y:A//B(x;y), x,y. t(x;y), , qeq(r;s), tt, x:AB(x), {i..j}, , {x:A| B(x)} , i  j < k, A  B, P & Q, A, False, P  Q, EquivRel(T;x,y.E(x;y)), s = t, , A  B, x:A  B(x), , , x:A. B(x), t  T, , rv-const(a), SQType(T), {T}, s ~ t, P  Q, P  Q, Void, X  Y, suptype(S; T), S  T, Dec(P), P  Q, left + right, A c B, a  b, case b of inl(x) => s(x) | inr(y) => t(y), isint(z;a;b), r < s, a < b, r + s, rv-partial-sum(n;i.X(i)), n - m, n+m, -n, i  j , x.A(x), (r) i  k < j. E(k),  lb  i < ub. E(i), *, r+gp, e, +r, <+*>, 0, i <z j, x f y, a  j < b. E(j), X + Y, q*X, X * Y, x:A.B(x), b, a  b, r - s, if b then t else f fi

Lemmas

qmul preserves qle, qadd-add, rv-disjoint-rv-scale, qle-int, qsub-sub, qsub wf, qle transitivity qorder, qadd inv assoc q, qinverse q, qadd preserves qle, qmul assoc, qmul over minus qrng, qinv inv q, qmul one qrng, int-eq-in-rationals, expectation-non-neg, non-neg-qmul, qmul functionality wrt qle, qadd functionality wrt qle, qle functionality wrt implies, qsum-const, expectation-qsum, rv-disjoint-symmetry, expectation-monotone-in-first, assert-qeq, expectation-rv-scale, rv-disjoint-monotone-in-first, rv-disjoint-rv-partial-sum, not wf, rv-disjoint-compose, expectation-rv-disjoint, rv-mul wf, rv-scale wf, rv-add wf, expectation-rv-add, top wf, q distrib, mon assoc q, qadd ac 1 q, qmul assoc qrng, qmul ident, qmul ac 1 qrng, qmul comm qrng, qadd comm q, rv-partial-sum wf, sum unroll hi q, qmul zero qrng, int-rational, expectation-constant, qadd wf, mon ident q, qmul over plus qrng, qsum wf, ge wf, qle weakening lt qorder, qle complement qorder, qle weakening eq qorder, decidable qle, q-square-non-neg, rv-const wf, expectation-monotone, expectation-rv-const, qle wf, rationals wf, int nzero wf, b-union wf, btrue wf, qeq wf2, bool wf, quotient wf, p-outcome wf, nat wf, length wf nat, le wf, true wf, squash wf, int seg wf, subtype rel function, nat properties, int seg properties, finite-prob-space wf, random-variable wf, qmul wf, rv-compose wf, expectation wf, int inc rationals, rv-disjoint wf